k:Knd, f, g:Top. islocal(k)  (kindcase(k; a.f(a); l,t.g(l,t) ) ~ f(act(k))) 

latex

Definitions	Knd, kindcase(k; a.f(a); l,t.g(l;t) ), b, islocal(k), act(k), lnk(k), tag(k), False, x:A. B(x), P  Q, True, t  T, Top
Lemmas	top wf, true wf, false wf, Knd wf